package joc.nextgen;

import static joc.nextgen.JOC.post;
import static joc.nextgen.JOC.result;

public class PointSpecContract implements PointSpec {

	@Invariant
	public void invariant() {
		assert getX() >= 0 : "x >= 0";
		assert getY() >= 0 : "y >= 0";
	}

	@Override
	public int getX() {
		if (post()) {
			assert result(int.class) >= 0 : "result >= 0";
		}
		return 0;
	}

	@Override
	public int getY() {
		if (post()) {
			assert result(int.class) >= 0 : "result >= 0";
		}
		return 0;
	}

}
